An open system is one in which only some of the system components are present. Of particular interest are so-called open concurrent reactive systems. It is important to be able to check the correctness of such open systems. Recently, systematic state-space exploration has been proposed as a tool to effect such checking of the open systems. Tools have evolved that extend systematic state-space exploration to concurrent reactive systems in which processes execute arbitrary code written in general-purpose programming languages, for example, C or C++.
However, such systematic state-space exploration requires that the open system being checked, i.e., analyzed, be "closed", i.e., self-executable. This of course implies that for a particular open reactive system, an executable representation of the environment in which the open system operates has to be available in order to close the system. Heretofore, such a representation of the open system environment was generated manually, which is typically a very difficult, time consuming and error prone task.
The representation of the open system environment, whether generated manually or even automatically, might be too restrictive and, thereby, cause the state-space exploration to miss possible erroneous behavior of the open system being analyzed. On the other hand, the resulting representation of the open system environment might be too general, thereby, increasing the size of the state-space, which may result in yielding spurious erroneous behaviors of the system being analyzed.